Nuprl Lemma : es-stable_wf
11,40
postcript
pdf
es
:ES,
i
:Id,
P
:(discrete state@
i
). @
i
stable
state
.
P
(
state
)
latex
Definitions
t
T
,
True
,
T
,
ES
,
Id
,
x
:
A
.
B
(
x
)
,
discrete state@
i
,
x
(
s
)
,
(discrete state after
e
)
,
(discrete state when
e
)
,
{
x
:
A
|
B
(
x
)}
,
Type
,
,
x
:
A
B
(
x
)
,
loc(
e
)
,
s
=
t
,
E
,
f
(
a
)
,
P
Q
,
x
.
t
(
x
)
,
e
@
i
.
P
(
e
)
,
@
i
stable
state
.
P
(
state
)
Lemmas
alle-at
wf
,
es-E
wf
,
es-loc
wf
,
es-dstate-when
wf
,
es-dstate-after
wf
,
es-dstate
wf
,
squash
wf
,
true
wf
,
Id
wf
,
event
system
wf
origin
es:ES, i:Id, P:(discrete state@i
). @i stable state.P(state) 
es:ES, i:Id, P:(discrete state@i). @i stable state.P(state) T
Tx:A. B(x)B(x)
Q
x. t(x)e@i. P(e)